
Axiom P Q R T : Prop.

Theorem Curry_Howard_1:
(P->Q) -> (Q->R) -> P -> R.
Proof.
exact (fun (H:P->Q) (H':Q->R) (p:P) => H' (H p)).
Qed.

Theorem Curry_Howard_2:
(P->Q)->(Q->R)->P->R.
Proof.
intros H' H p.
exact (H (H' p)).
Qed.

Definition Curry_Howard_3 := fun (H:P->Q) (H':Q->R) (p:P) => H' (H p).
Definition Curry_Howard_4 (H:P->Q) (H':Q->R) (p:P) : R := H' (H p).

Print Curry_Howard_1.
Print Curry_Howard_2.
Print Curry_Howard_3.
Print Curry_Howard_4.
